This invention relates generally to analysis of computer programs for defects, and more particularly an improved weakest precondition analysis of computer programs for such defects.
Computer programs have become increasingly complex. A modem-day application program, such as a word processing program, developed for an operating system having a graphical user interface, such as a version of Microsoft Windows, can take many years to develop, with the joint efforts of a team of programmers. As a result, computer program analysis to identify defects in a program before it is released to the general public has become increasingly more important. Sophisticated analysis techniques have become available, to allow programmers to identify defects in their programs that may hinder the performance of the programs, or may even cause the programs to crash, reducing their reliability.
One such computer program analysis technique is known as weakest precondition analysis. This is a type of program analysis that precisely tracks the algebraic properties of program variables (typically expressed as functions of other program variables) both before and after every statement in the program being analyzed. It is much more powerful than other program analysis techniques which keep track of only very simple properties of program variables (e.g. whether the variable contains a constant value).
A disadvantage with weakest precondition analysis, however, is that it generally requires a large amount of computer memory to analyze large programs, and thus may also require long periods of time to conduct the analysis. This reduces its usefulness for programmers, to the extent that they may not use weakest precondition analysis because of its time and memory constraints. For these and other reasons, there is a need for the present invention.
The invention provides for a considerable reduction in the time and memory required to analyze computer programs using weakest precondition analysis of computer programs. In one embodiment, a computer-implemented method includes first identifying a set of candidates of a computer program that are potentially defective, via a predetermined data flow analysis. As used herein, the term data flow analysis is coextensive with the terms program analysis and program structure analysis, such that either can be substituted for the term data flow analysis. Next, each of these candidates is examined via a weakest precondition analysis to determine whether the candidate actually is defective.
In this manner, embodiments of the invention provide for improved weakest precondition analysis. The weakest precondition analysis is not conducted over the entire computer program, but rather as to only those candidates within the computer program that have already been determined to be potentially defective. Desirably, the predetermined data flow analysis to determine such potentially defective candidates is a much quicker analysis than weakest precondition analysis. Thus, the initial identification of a set of candidates that are potentially defective means that the weakest precondition analysis will only be run as to those candidates that may be defectivexe2x80x94and not, in other words, as to those candidates that are for certain not defective (as determined by the predetermined data flow analysis). This results in an analysis of the computer program that is relatively fast, but still utilizes weakest precondition analysis.
The invention includes systems, methods, computers, and computer-readable media of varying scope. Besides the embodiments, advantages and aspects of the invention described here, the invention also includes other embodiments, advantages and aspects, as will become apparent by reading and studying the drawings and the following description.